HW#1 --- last modified February 07 2019 23:07:54..

Solution set.

Due date: 1_DATE

Files to be submitted:
  Hw4.zip

Purpose:

Related Course Outcomes:

The main course outcomes covered by this assignment are:

LO2 -- By code or by hand translate sentences in first-order logic to conjunctive normal form (CNF).

LO3 -- By code or by hand find proofs by using resolution.

LO9 -- Students should be able to explain the advantages and disadvantages of the STRIPS representation for planning.

LO10 -- Students should be able to describe the frame problem.

LO11 -- Students should be able to describe default reasoning.

Specification:

For this homework, I want you to write up solutions to the following five problems and put them into a file Hw1.pdf. If you are taking CS286 I also want you to write an at least one page book report on the paper "Mick gets some" by Chvatal and Reed. I want you to discuss the algorithms they present to find satisfying assignment when one is beneath the threshold and any connections they may have to DPLL. Except for the book report you can work in teams of 2-3. The book report must be done alone.

1. On April 4, we discussed a simple logic for the natural numbers. For the first problem I would like you to fully and formally specify an extension of this logic to include lists of natural numbers. In English (not formally), a list satisfies: (a) An empty list is a list. (b) If x is a natural number and y is a list then adding x to the front of y is a list. (c) If y is a list and not the empty list, then the first element of y is a natural number. (d) If y is a list and not the empty list, then there is a natural number x and a list z such that such that adding x to the front of z is the same as the list y. Once have written your axioms, rewrite them in prenex normal form, such that within the quantifiers the formula is in conjunctive normal form.
2. Express the following formula in your first-order logic from problem (1): For any list y, there exists a list x, whose first five elements are the number 1, and the rest of x is y. Carefully, using Tarski's definition of truth show this formula is valid in any model that satisfies your axioms. Skolemize this formula and your axioms, and try to give a resolution proof for it.
3. Draw the planning graph for the problem in Figure 10.2 in the book. Solve the problem step-by-step using the GraphPlan algorithm.
4. Briefly explain how PDDL solves the frame problem. Give some disadvantages to formulating problems in PDDL.
5. Come up with four toy examples of default rules. Your `n`th example should have exactly n distinct extensions.

Point Breakdown